p:FinProbSpace, n:, X, Y, Z:RandomVariable(p;n).
rv-disjoint(p;n;X;Y)  rv-disjoint(p;n;X;Z)  rv-disjoint(p;n;X;Y * Z) 

latex

Definitions	t  T, P  Q, x:A. B(x), True, f(a), <a, b>, , s = t, False, A, P & Q, A  B, i  j < k, , {x:A| B(x)} , , {i..j}, T, r * s, Outcome, x:AB(x), #$n, Type, , X * Y, S  T, RandomVariable(p;n), suptype(S; T), {T}, P  Q, left + right, rv-disjoint(p;n;X;Y), FinProbSpace
Lemmas	rv-disjoint wf, random-variable wf, nat wf, finite-prob-space wf, rv-mul wf, not wf, int seg wf, p-outcome wf, qmul wf, squash wf, true wf, rationals wf